A, A':Type.
strong-subtype(A;A')
 (B:(AType), C:(A'Type), eq:EqDecider(A), eq':EqDecider(A'), f, g:a:A fp B(a).
 (a:A. B(a) r C(a))  f  g  f  g) 

latex

Definitions	x  dom(f), , t.2, f(x), {T}, Top, t  T, EqDecider(T), a:A fp B(a), strong-subtype(A;B), A c B, x. t(x), x(s), f  g, x:A. B(x), P  Q, b
Lemmas	fpf-sub wf, strong-subtype-deq-subtype, fpf wf, deq wf, strong-subtype wf, strong-subtype-self, fpf-trivial-subtype-top, fpf-dom-type2, fpf-dom functionality2, fpf-ap wf, fpf-dom wf, assert wf